Search Results

Documents authored by Igarashi, Atsushi

Document
DOI: 10.4230/LIPIcs.ECOOP.2020.8
Space-Efficient Gradual Typing in Coercion-Passing Style

Authors: Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Herman et al. pointed out that the insertion of run-time checks into a gradually typed program could hamper tail-call optimization and, as a result, worsen the space complexity of the program. To address the problem, they proposed a space-efficient coercion calculus, which was subsequently improved by Siek et al. The semantics of these calculi involves eager composition of run-time checks expressed by coercions to prevent the size of a term from growing. However, it relies also on a nonstandard reduction rule, which does not seem easy to implement. In fact, no compiler implementation of gradually typed languages fully supports the space-efficient semantics faithfully. In this paper, we study coercion-passing style, which Herman et al. have already mentioned, as a technique for straightforward space-efficient implementation of gradually typed languages. A program in coercion-passing style passes "the rest of the run-time checks" around - just like continuation-passing style (CPS), in which "the rest of the computation" is passed around - and (unlike CPS) composes coercions eagerly. We give a formal coercion-passing translation from λS by Siek et al. to λS₁, which is a new calculus of first-class coercions tailored for coercion-passing style, and prove correctness of the translation. We also implement our coercion-passing style transformation for the Grift compiler developed by Kuhlenschmidt et al. An experimental result shows stack overflow can be prevented properly at the cost of up to 3 times slower execution for most partially typed practical programs.
Cite as

Yuya Tsuda, Atsushi Igarashi, and Tomoya Tabuchi. Space-Efficient Gradual Typing in Coercion-Passing Style. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 8:1-8:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tsuda_et_al:LIPIcs.ECOOP.2020.8,
  author =	{Tsuda, Yuya and Igarashi, Atsushi and Tabuchi, Tomoya},
  title =	{{Space-Efficient Gradual Typing in Coercion-Passing Style}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{8:1--8:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.8},
  URN =		{urn:nbn:de:0030-drops-131658},
  doi =		{10.4230/LIPIcs.ECOOP.2020.8},
  annote =	{Keywords: Gradual typing, coercion calculus, coercion-passing style, dynamic type checking, tail-call optimization}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.2
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions

Authors: Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
Context-aware applications, whose behavior reactively depends on the time-varying status of the surrounding environment - such as network connection, battery level, and sensors - are getting more and more pervasive and important. The term "context-awareness" usually suggests prompt reactions to context changes: as the context change signals that the current execution cannot be continued, the application should immediately abort its execution, possibly does some clean-up tasks, and suspend until the context allows it to restart. Interruptions, or asynchronous exceptions, are useful to achieve context-awareness. It is, however, difficult to program with interruptions in a compositional way in most programming languages because their support is too primitive, relying on synchronous exception handling mechanism such as try-catch. We propose a new domain-specific language ContextWorkflow for interruptible programs as a solution to the problem. A basic unit of an interruptible program is a workflow, i.e., a sequence of atomic computations accompanied with compensation actions. The uniqueness of ContextWorkflow is that, during its execution, a workflow keeps watching the context between atomic actions and decides if the computation should be continued, aborted, or suspended. Our contribution of this paper is as follows; (1) the design of a workflow-like language with asynchronous interruption, checkpointing, sub-workflows and suspension; (2) a formal semantics of the core language; (3) a monadic interpreter corresponding to the semantics; and (4) its concrete implementation as an embedded domain-specific language in Scala.
Cite as

Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 2:1-2:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{inoue_et_al:LIPIcs.ECOOP.2018.2,
  author =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  title =	{{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{2:1--2:33},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.2},
  URN =		{urn:nbn:de:0030-drops-92074},
  doi =		{10.4230/LIPIcs.ECOOP.2018.2},
  annote =	{Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
Document
DOI: 10.4230/DARTS.4.3.4
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)

Authors: Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
This artifact provides the Scala, Haskell, and Purescript implementations of ContextWorkflow, an embedded domain-specific language for interruptible and compensable executions, and demonstrates the maze search example described in the companion paper. The Haskell and Purescript implementations provide the core language constructs including \texttt{checkpoint} for partial aborts and \texttt{sub} for sub-workflows and show that ContextWorkflow can be embedded in eager and lazy languages as described in the companion paper. The Scala implementation does not only provide user-friendly syntax of ContextWorkflow but also gives the maze search example as an interactive GUI application.
Cite as

Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{inoue_et_al:DARTS.4.3.4,
  author =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  title =	{{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)}},
  pages =	{4:1--4:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.4.3.4},
  URN =		{urn:nbn:de:0030-drops-92356},
  doi =		{10.4230/DARTS.4.3.4},
  annote =	{Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact